<html>
<head><meta charset="utf-8"><title>Rust verification tools · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Rust.20verification.20tools.html">Rust verification tools</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="208996911"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Rust%20verification%20tools/near/208996911" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Rust.20verification.20tools.html#208996911">(Sep 03 2020 at 16:47)</a>:</h4>
<p>My team in Google Research has been thinking about what we want in Rust verification.<br>
We want to narrow the gap between testing and verification. e.g., by making it easy to switch back and forth between testing and verification.</p>
<p>So we have been reimplementing the proptest library so that you can use the same test harness for testing/fuzzing with proptest and for formal verification using automatic verification tools like KLEE.</p>
<p>It's early days yet but we have something that works and we would love feedback on whether this is a direction that the community should go in or not.</p>
<p>Code: <a href="https://github.com/project-oak/rust-verification-tools">https://github.com/project-oak/rust-verification-tools</a><br>
Blog post: <a href="https://alastairreid.github.io/why-not-both/">https://alastairreid.github.io/why-not-both/</a><br>
Tweet: <a href="https://twitter.com/alastair_d_reid/status/1301543693233655810">https://twitter.com/alastair_d_reid/status/1301543693233655810</a></p>
<div class="inline-preview-twitter"><div class="twitter-tweet"><a href="https://twitter.com/alastair_d_reid/status/1301543693233655810"><img class="twitter-avatar" src="https://pbs.twimg.com/profile_images/731458319433519104/q1EULfSQ_normal.jpg"></a><p>Verifying vs testing?  Why not both?
New blog post about our work on Rust verification based on reimplementing the proptest library for formal verification tools so you can use the same test harness with both proptest and with “propverify”.
<a href="https://twitter.com/rustlang">@rustlang</a> #KLEE
<a href="https://t.co/rAzAvW6MCI">https://alastairreid.github.io/why-not-both/</a></p><span>- Alastair Reid (@alastair_d_reid)</span></div></div>



<a name="208997420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Rust%20verification%20tools/near/208997420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Rust.20verification.20tools.html#208997420">(Sep 03 2020 at 16:51)</a>:</h4>
<p>It shows a double scroll bar on code blocks in Firefox on Linux:</p>
<p><a href="/user_uploads/4715/phAyFXyFpAP8CF4N0wx2lPLo/image.png">image.png</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/phAyFXyFpAP8CF4N0wx2lPLo/image.png" title="image.png"><img src="/user_uploads/4715/phAyFXyFpAP8CF4N0wx2lPLo/image.png"></a></div><p>This is likely caused by the <code>overflow: scroll</code> instead of <code>overflow: auto</code>.</p>



<a name="209000233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Rust%20verification%20tools/near/209000233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Rust.20verification.20tools.html#209000233">(Sep 03 2020 at 17:12)</a>:</h4>
<p>Ugh! That is horrible. I guess I have to go futz with my website a bit. Thanks for the diagnosis!</p>



<a name="209071705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Rust%20verification%20tools/near/209071705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Rust.20verification.20tools.html#209071705">(Sep 04 2020 at 09:22)</a>:</h4>
<p>I fully agree with the point of this post. :) Testing and verification can complement each other very well.</p>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> some of this would also be very interesting to the secure code WG (<a class="stream" data-stream-id="146229" href="/#narrow/stream/146229-wg-secure-code">#wg-secure-code</a>), just in case you are not yet familiar with their work.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>